Program verifications such as inferring efficient synchronization in concurrent programs are tasks known to be difficult and error-prone when done manually. Existing approaches include uses of temporal specifications to generate synchronization skeletons. Other works consider the problem of program repair as a game.
The problem of restricting the program to valid executions can be addressed by monitoring the program at runtime and forcing it to avoid executions that violate the specification. However, restricting the executions of a program at runtime requires a recovery mechanism in case the program already performed a step that violates the specification, and/or a predictive mechanism to check whether future steps lead to a violation. Existing approaches using recovery mechanisms typically require user annotations to define a corrective action to be taken when the specification is violated.